@string { SCIENCE = "Science" }
@string { LNCS = "LNCS" }
@string { ACM = "ACM" }
@string { AI = "Artificial Intelligence" }
@string { AIM = "{AI} Magazine"}
@string { AICOM = "{AI} Communications" }
@string { CONSTRAINTS = "Constraints" }
@string { SV = "Springer" }
@string { IEEETRANC = "IEEE Transactions on Computers" }
@string { IEEEP = "IEEE Press" }
@string { JSAT = "Journal on Satisfiability Boolean Modeling and Computation" }
@string { JSC = "Journal of Symbolic Computation"}
@string { AMAI = "Annals of Mathematics and Artificial Intelligence"}
@string { FI = "Fundamenta Informaticae" }

@inproceedings{RakadjievSMO15,
  author    = {Emil Rakadjiev and
               Taku Shimosawa and
               Hiroshi Mine and
               Satoshi Oshima},
  title     = {Parallel {SMT} Solving and Concurrent Symbolic Execution},
  booktitle = {2015 {IEEE} TrustCom/BigDataSE/ISPA, Helsinki, Finland, August 20-22, 2015, Volume 3},
  pages     = {17--26},
  year      = {2015},
  OPTurl       = {http://dx.doi.org/10.1109/Trustcom.2015.608},
  doi       = {10.1109/Trustcom.2015.608},
  timestamp = {Fri, 11 Dec 2015 14:36:57 +0100},
}

@inproceedings{AsadiBFHESC18,
  author    = {Sepideh Asadi and
               Martin Blicha and
               Grigory Fedyukovich and
               Antti E. J. Hyv{\"{a}}rinen and
               Karine Even{-}Mendoza and
               Natasha Sharygina and
               Hana Chockler},
  title     = {Function Summarization Modulo Theories},
  booktitle = {{LPAR-22.} 22nd International Conference on Logic for Programming,
               Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November
               2018},
  pages     = {56--75},
  year      = {2018},
  publisher = {EasyChair},
  series    = {EPiC Series in Computing},
  volume    = {57},
}

@inproceedings{MarescottiHS16,
  author    = {Matteo Marescotti and
               Antti E. J. Hyv{\"{a}}rinen and
               Natasha Sharygina},
  title     = {Clause Sharing and Partitioning for Cloud-Based {SMT} Solving},
  booktitle = {Automated Technology for Verification and Analysis - 14th International
               Symposium, {ATVA} 2016, Chiba, Japan, October 17-20, 2016, Proceedings},
  pages     = {428--443},
  year      = {2016},
}

@inproceedings{HyvarinenMSCS18,
  author    = {Antti E. J. Hyv{\"{a}}rinen and
               Matteo Marescotti and
               Parvin Sadigova and
               Hana Chockler and
               Natasha Sharygina},
  title     = {Lookahead-Based {SMT} Solving},
  booktitle = {Proc.~LPAR-22},
  OPTbooktitle = {{LPAR-22.} 22nd International Conference on Logic for Programming,
               Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November
               2018},
  pages     = {418--434},
  year      = {2018},
  publisher = {EasyChair},
  series    = {EPiC Series in Computing},
  volume    = {57},
}

@inproceedings{MarescottiHS18,
  author    = {Matteo Marescotti and
               Antti E. J. Hyv{\"{a}}rinen and
               Natasha Sharygina},
  title     = {{SMTS:} Distributed, Visualized Constraint Solving},
  booktitle = {Proc.~LPAR-22},
  OPTbooktitle = {{LPAR-22.} 22nd International Conference on Logic for Programming,
               Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November
               2018},
  pages     = {534--542},
  year      = {2018},
  publisher = {EasyChair},
  series    = {EPiC Series in Computing},
  volume    = {57},
}

@inproceedings{JancikAFHKS16,
  author    = {Pavel Janc{\'{\i}}k and
               Leonardo Alt and
               Grigory Fedyukovich and
               Antti E. J. Hyv{\"{a}}rinen and
               Jan Kofron and
               Natasha Sharygina},
  title     = {{PVAIR:} Partial Variable Assignment InterpolatoR},
  booktitle = {Fundamental Approaches to Software Engineering - 19th International
               Conference, {FASE} 2016, Held as Part of the European Joint Conferences
               on Theory and Practice of Software, {ETAPS} 2016, Eindhoven, The Netherlands,
               April 2-8, 2016, Proceedings},
  pages     = {419--434},
  year      = {2016},
}

@inproceedings{AltHAS17,
  author    = {Leonardo Alt and
               Antti Eero Johannes Hyv{\"{a}}rinen and
               Sepideh Asadi and
               Natasha Sharygina},
  title     = {Duality-based interpolation for quantifier-free equalities and uninterpreted
               functions},
  booktitle = {2017 Formal Methods in Computer Aided Design, {FMCAD} 2017, Vienna,
               Austria, October 2-6, 2017},
  pages     = {39--46},
  year      = {2017},
}

@inproceedings{BlichaHKS19,
  author    = {Martin Blicha and
               Antti E. J. Hyv{\"{a}}rinen and
               Jan Kofron and
               Natasha Sharygina},
  title     = {Decomposing {Farkas} Interpolants},
  booktitle = {Proc.~TACAS 2019},
  OPTbooktitle = {Tools and Algorithms for the Construction and Analysis of Systems
               - 25th International Conference, {TACAS} 2019, Held as Part of the
               European Joint Conferences on Theory and Practice of Software, {ETAPS}
               2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part
               {I}},
  pages     = {3--20},
  year      = {2019},
  series    = LNCS,
  volume    = {11427},
  publisher = SV,

}

@inproceedings{AltACMFHS17,
  author    = {Leonardo Alt and
               Sepideh Asadi and
               Hana Chockler and
               Karine Even{-}Mendoza and
               Grigory Fedyukovich and
               Antti E. J. Hyv{\"{a}}rinen and
               Natasha Sharygina},
  title     = {{HiFrog}: {SMT}-based Function Summarization for Software Verification},
  booktitle = {Proc.~TACAS 2017},
  OPTbooktitle = {Tools and Algorithms for the Construction and Analysis of Systems
               - 23rd International Conference, {TACAS} 2017, Held as Part of the
               European Joint Conferences on Theory and Practice of Software, {ETAPS}
               2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part {II}},
  pages     = {207--213},
  year      = {2017},
  series    = LNCS,
  publisher = SV,
  volume    = {10206},
}

@inproceedings{HyvarinenMAS16,
  author    = {Antti E. J. Hyv{\"{a}}rinen and
               Matteo Marescotti and
               Leonardo Alt and
               Natasha Sharygina},
  title     = {{OpenSMT2}: An {SMT} Solver for Multi-core and Cloud Computing},
  booktitle = {Proc.~SAT 2016},
  OPTbooktitle = {Theory and Applications of Satisfiability Testing - {SAT} 2016 - 19th
               International Conference, Bordeaux, France, July 5-8, 2016, Proceedings},
  pages     = {547--553},
  year      = {2016},
  publisher = SV,
  volume    = {9710},
  series    = LNCS,
}

@inproceedings{Holzmann:VMCAI16,
  author    = {Gerard J. Holzmann},
  title     = {Cloud-Based Verification of Concurrent Software},
  booktitle = {Verification, Model Checking, and Abstract Interpretation - 17th International Conference, {VMCAI} 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings},
  pages     = {311--327},
  year      = {2016},
  url       = {http://dx.doi.org/10.1007/978-3-662-49122-5_15},
  doi       = {10.1007/978-3-662-49122-5_15},
  timestamp = {Tue, 05 Jan 2016 12:40:34 +0100},
}

@inproceedings{BalyoSS:SAT15,
  author    = {Tomas Balyo and
               Peter Sanders and
               Carsten Sinz},
  title     = {HordeSat: {A} Massively Parallel Portfolio {SAT} Solver},
  booktitle = {Theory and Applications of Satisfiability Testing - {SAT} 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015. Proceedings},
  pages     = {156--172},
  year      = {2015},
  url       = {http://dx.doi.org/10.1007/978-3-319-24318-4_12},
  doi       = {10.1007/978-3-319-24318-4_12},
  timestamp = {Thu, 17 Sep 2015 13:26:14 +0200},
}

@inproceedings{HyvarinenMS:SAT15,
  author    = {Antti E. J. Hyv{\"{a}}rinen and
               Matteo Marescotti and
               Natasha Sharygina},
  title     = {Search-Space Partitioning for Parallelizing {SMT} Solvers},
  booktitle = {Proc.~SAT 2015},
  OPTbooktitle = {Theory and Applications of Satisfiability Testing, {SAT} 2015, 18th International Conference, Austin, TX, USA, September 24-27, 2015. Proceedings},
  pages     = {369--386},
  year      = {2015},
  OPTurl       = {http://dx.doi.org/10.1007/978-3-319-24318-4_27},
  doi       = {10.1007/978-3-319-24318-4_27},
  timestamp = {Thu, 17 Sep 2015 13:26:14 +0200},
  series    = LNCS,
  publisher = SV,
  volume    = {9340},
}

@inproceedings{Manthey:PoS2011,
  author        = {Norbert Manthey},
  title         = {Parallel {SAT} Solving -- Using More Cores},
  booktitle     = {Easychair Proceedings of the 2nd Pragmatics of SAT
                   Wokshop (PoS11)},
  year          = {2011},
  pages         = {1--14},

}

@inproceedings{EenS:SAT03,
  author        = {Niklas E{\'e}n and Niklas S{\"o}rensson},
  title         = {An Extensible {SAT}-solver},
  booktitle     = {Proc.~SAT 2004},
  publisher     = SV,
  series        = LNCS,
  volume        = {2919},
  year          = {2004},
  pages         = {502--518},
}

@inproceedings{MoskewiczMZZM:DAC01,
  author        = {Matthew W. Moskewicz and Conor F. Madigan and Ying
                   Zhao and Lintao Zhang and Sharad Malik},
  title         = {Chaff: Engineering an Efficient {SAT} Solver},
  booktitle     = {Proc.~DAC 2001},
  publisher     = ACM,
  year          = {2001},
  pages         = {530--535},
}

@inproceedings{HolldoblerMS:LPAR2010,
  author        = {Steffen H{\"o}lldobler and Norbert Manthey and Ari
                   Saptawijaya},
  title         = {Improving Resource-Unaware {SAT} Solvers},
  booktitle     = {Proc.~LPAR 2010},
  publisher     = SV,
  series        = LNCS,
  volume        = {6397},
  year          = {2010},
  pages         = {519 -- 534},
}

@techreport{Biere:2010,
  author        = {Armin Biere},
  title         = {{Lingeling}, {Plingeling}, {PicoSAT} and {PrecoSAT}
                   at {SAT} race 2010},
  institution   = {Institute for Formal Models and Verification,
                   Johannes Kepler University},
  address       = {Altenbergenstr. 69, 4040 Linz, Austria},
  series        = {Technical Report 10/1},
  month         = AUG,
  year          = {2010},
}


@inproceedings{WintersteigerHM:CAV09,
  author    = {Christoph M. Wintersteiger and
               Youssef Hamadi and
               Leonardo Mendon{\c{c}}a de Moura},
  title     = {A Concurrent Portfolio Approach to {SMT} Solving},
  OPTbooktitle = {Computer Aided Verification, 21st International
        Conference, {CAV} 2009, Grenoble, France, June 26 - July 2,
        2009.  Proceedings},
  booktitle = {Proc.~CAV 2009},
  year      = {2009},
  pages     = {715--720},
  series    = LNCS,
  volume    = {5643},
  publisher = SV,
}

@inproceedings{PalikarevaC:CAV13,
  author    = {Hristina Palikareva and
               Cristian Cadar},
  title     = {Multi-solver Support in Symbolic Execution},
  OPTbooktitle = {Computer Aided Verification - 25th International
               Conference, {CAV} 2013, Saint Petersburg, Russia, July
               13-19, 2013.  Proceedings},
  booktitle = {Proc.~CAV 2013},
  year      = {2013},
  pages     = {53--68},
  series    = LNCS,
  volume    = {8044},
  publisher = SV,
}

@inproceedings{BruttomessoPST:TACAS10,
 author = {Roberto Bruttomesso and Edgar Pek and Natasha Sharygina and
            Aliaksei Tsitovich},
 title  = {The {OpenSMT} Solver},
 OPTbooktitle = {Tools and Algorithms for the Construction and Analysis of
     Systems, 16th International Conference, {TACAS} 2010, Held as Part
     of the Joint European Conferences on Theory and Practice of
     Software, {ETAPS} 23010, Paphos, Cyprus, March 20 -- 28, 2010.
     Proceedings},
 booktitle = {Proc.~TACAS 2010},
 year   = {2010},
 pages  = {150--153},
 series = LNCS,
 volume = {6015},
 publisher = {Springer},
}

@inproceedings{NieuwenhuisO:RTA05,
    author      = {Robert Nieuwenhuis and Albert Oliveras},
    title       = {Proof-Producing Congruence Closure},
    OPTbooktitle   = {Term Rewriting and Applications, 16th International
                   Conference, RTA 2005, Nara, Japan, April 19--21, 2005,
                   Proceedings},
    booktitle   = {Proc.~RTA 2005},
    year        = {2005},
    pages       = {453 -- 468},
    publisher   = SV,
    series      = LNCS,
    volume      = {3467},
}

@inproceedings{SorenssonEen:SAT2003,
  author    = {Niklas E{\'e}n and
               Niklas S{\"o}rensson},
  title     = {An Extensible {SAT}-solver},
  booktitle = {Proc.\ SAT'03},
  OPTbooktitle     = {Proceedings of the 6th International Conference on
                      Theory and Applications of Satisfiability Testing
                      (SAT 2003), Selected Revised Papers},
  OPTbooktitle = {Theory and Applications of Satisfiability Testing},
  OPTeditor    = {Enrico Giunchiglia and
               Armando Tacchella},
  year      = {2004},
  pages     = {502--518},
  publisher = SV,
  series    = LNCS,
  volume    = {2919},
  OPTcrossref  = {SAT2003},
}


@article{DetlefsNS:JACM05,
  author    = {David Detlefs and
               Greg Nelson and
               James B. Saxe},
  title     = {Simplify: a theorem prover for program checking},
  journal   = {Journal of the ACM},
  year      = {2005},
  volume    = {52},
  number    = {3},
  pages     = {365--473},
}

@article{DavisLL:ACM1962,
  author    = {Martin Davis and
               George Logemann and
               Donald W. Loveland},
  title     = {A machine program for theorem-proving},
  journal   = {Commun. {ACM}},
  volume    = {5},
  number    = {7},
  pages     = {394--397},
  year      = {1962},
  url       = {http://doi.acm.org/10.1145/368273.368557},
  doi       = {10.1145/368273.368557},
  timestamp = {Thu, 20 Nov 2003 13:05:43 +0100},
}

@article{NieuwenhuisOT:JACM06,
  author    = {Robert Nieuwenhuis and Albert Oliveras and Cesare
               Tinelli},
  title     = {Solving {SAT} and {SAT} Modulo Theories: From an abstract
               {Davis}--{Putnam}--{Logemann}--{Loveland} procedure to
               {DPLL(T)}},
  journal   = {Journal of the ACM},
  year      = {2006},
  volume    = {53},
  number    = {6},
  pages     = {937 -- 977},
}

@inproceedings{AlbertiBGRS:CAV12,
  author    = {Francesco Alberti and
               Roberto Bruttomesso and
               Silvio Ghilardi and
               Silvio Ranise and
               Natasha Sharygina},
  title     = {{SAFARI:} {SMT}-Based Abstraction for Arrays with
                Interpolants},
  OPTbooktitle = {Computer Aided Verification - 24th International
                Conference, {CAV}
                2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings},
  booktitle = {Proc.~CAV 2012},
  year      = {2012},
  pages     = {679--685},
  series    = LNCS,
  volume    = {7358},
  publisher = SV,
}

@inproceedings{LiAKGC:POPL14,
  author    = {Yi Li and
               Aws Albarghouthi and
               Zachary Kincaid and
               Arie Gurfinkel and
               Marsha Chechik},
  title     = {Symbolic optimization with {SMT} solvers},
  OPTbooktitle = {The 41st Annual {ACM} {SIGPLAN-SIGACT} Symposium on
                  Principles of Programming Languages, {POPL} '14, San
                  Diego, CA, USA, January 20-21, 2014},
  booktitle = {Proc.~POPL 2014},
  year      = {2014},
  pages     = {607--618},
  publisher = ACM,
}

@inproceedings{NieuwenhuisO:SAT06,
  author    = {Robert Nieuwenhuis and Albert Oliveras},
  title     = {On {SAT} Modulo Theories and Optimization Problems},
  OPTbooktitle = {Theory and Applications of Satisfiability Testing - {SAT}
                  2006, 9th International Conference, Seattle, WA, USA,
                  August 12-15, 2006, Proceedings},
  booktitle = {Proc.~SAT 2006},
  year      = {2006},
  pages     = {156--169},
  series    = LNCS,
  volume    = {4121},
  publisher = SV,
}


@inproceedings{BarretCDHJKRT:CAV11,
 author = {Clark Barrett and Christopher L. Conway and Morgan Deters and
             Liana Hadarean and Dejan Jovanovic and Tim King and Andrew
             Reynolds and Cesare Tinelli},
 title  = {{CVC4}},
 OPTbooktitle = {Computer Aided Verification --- 23rd International
             Conference, {CAV} 2011, Snowbird, UT, USA, July 14 -- 20,
             2011.  Proceedings},
 booktitle = {Proc.~CAV 2011},
 year   = {2011},
 pages  = {171 -- 177},
 series = LNCS,
 volume = {6806},
 publisher = {Springer},
}

@inproceedings{Dutertre:CAV14,
 author = {Bruno Dutertre},
 title  = {Yices 2.2},
 OPTbooktitle = {Computer Aided Verification --- 26th International
             Conference, {CAV} 2014, Held as Part of the Vienna Summer
             of Logic, {VSL} 2014, Vienna, Austria, July 18 -- 22, 2014.
             Proceedings},
 booktitle = {CAV 2014},
 year   = {2014},
 pages  = {737 -- 744},
 volume = {8599},
 publisher = {Springer},
 series = LNCS,
}

@inproceedings{CimattiGSS:TACAS13,
 author = {Alessandro Cimatti and Alberto Griggio and Bastiaan Joost
            Schaafsma and Roberto Sebastiani},
 title  = {The {MathSAT5} {SMT} Solver},
 OPTbooktitle = {Tools and Algorithms for the Construction and Analysis of
             Systems --- 19th International Conference, {TACAS} 2013,
             Held as Part of the European Joint Conferences on Theory
             and Practice of Software, {ETAPS} 2013, Rome, Italy, March
             16 -- 24, 2013.  Proceedings},
 booktitle = {Proc.~TACAS 2013},
 year   = {2013},
 pages  = {93 -- 107},
 series = LNCS,
 publisher = {Springer},
 volume = {7795},
}

@inproceedings{MouraB:TACAS08,
 author = {Leonardo Mendon{\c{c}}a de Moura and Nikolaj Bj{\o}rner},
 title  = {{Z3:} An Efficient {SMT} Solver},
 OPTbooktitle = {Tools and Algorithms for the Construction and Analysis of
         Systems, 14th International Conference, {TACAS} 2008, Held as
         Part of the Joint European Conferences on Theory and Practice
         of Software, {ETAPS} 2008, Budapest, Hungary, March 29 -- April
         6, 2008.  Proceedings},
 booktitle = {Proc.~TACAS 2008},
 year   = {2008},
 pages  = {337 -- 340},
 series = LNCS,
 volume = {4963},
 publisher = {Springer},
}

@article{MarquesSilvaS:IEEETRANC99,
  author    = {Jo{\~a}o P. Marques-Silva and
               Karem A. Sakallah},
  title     = {{GRASP}: A Search Algorithm for Propositional Satisfiability},
  journal   = IEEETRANC,
  volume    = {48},
  number    = {5},
  year      = {1999},
  pages     = {506--521},
  OPTpublisher = IEEEP,
}

@phdthesis{Hyvarinen:PhD,
  author    = {Antti E. J. Hyv\"{a}rinen},
  title     = {Grid-Based Propositional Satisfiability Solving},
  school    = {Aalto University School of Science},
  year      = {2011},
  month     = {11},
  number    = {DD118/2011},
  address   = {Aalto Print, Helsinki, Finland},
}

@inproceedings{HyvarinenM:SAT2012,
  author    = {Antti Eero Johannes Hyv{\"{a}}rinen and
               Norbert Manthey},
  title     = {Designing Scalable Parallel {SAT} Solvers},
  OPTbooktitle = {Theory and Applications of Satisfiability Testing - {SAT}
                    2012 - 15th International Conference, Trento, Italy, June 17-20,
                    2012. Proceedings},
  booktitle = {Proc.~SAT 2012},
  year      = {2012},
  pages     = {214--227},
  series    = LNCS,
  volume    = {7317},
  publisher = SV,
}

@article{HamadiJS_09,
  author    = {Youssef Hamadi and Said Jabbour and Lakhdar Sais},
  title     = {{ManySAT}: a Parallel {SAT} Solver},
  journal   = JSAT,
  volume    = {6},
  number    = {4},
  year      = {2009},
  pages     = {245 -- 262},
}

@inproceedings{AudemardHJP:POS14,
  author    = {Gilles Audemard and Beno\^it Hoessen and Sa\"id Jabbour
                and C\'edric Piette},
  title     = {Dolius: A Distributed Parallel {SAT} Solving Framework},
  booktitle = {POS-14},
  OPTeditor    = {Daniel Le Berre},
  series    = {EPiC Series},
  volume    = {27},
  pages     = {1-11},
  year      = {2014},
  publisher = {EasyChair},
  bibsource = {EasyChair, http://www.easychair.org},
  issn      = {2040-557X},
}

@inproceedings{KatsirelosSSS:AAAI2013,
  author    = {George Katsirelos and
               Ashish Sabharwal and
               Horst Samulowitz and
               Laurent Simon},
  title     = {Resolution and Parallelizability: Barriers to the
                Efficient Parallelization of {SAT} Solvers},
  OPTbooktitle = {Proceedings of the Twenty-Seventh {AAAI} Conference on
  Artificial Intelligence, July 14-18, 2013, Bellevue, Washington,
  {USA.}},
  booktitle = {Proc.~AAAI 2013},
  year      = {2013},
  OPTeditor    = {Marie desJardins and
               Michael L. Littman},
  publisher = {{AAAI} Press},
}

@article{HamadiW:2013,
  author    = {Youssef Hamadi and
               Christoph M. Wintersteiger},
  title     = {Seven Challenges in Parallel {SAT} Solving},
  journal   = AIM,
  year      = {2013},
  volume    = {34},
  number    = {2},
  pages     = {99--106},
}

@article{MartinsML:2012,
  author    = {Ruben Martins and
               Vasco M. Manquinho and
               In{\^{e}}s Lynce},
  title     = {An overview of parallel {SAT} solving},
  journal   = CONSTRAINTS,
  year      = {2012},
  volume    = {17},
  number    = {3},
  pages     = {304--347},
}

@inproceedings{BjornerPF:TACAS15,
  author    = {Nikolaj Bj{\o}rner and Anh{-}Dung Phan and Lars Fleckenstein},
  title     = {{\(\nu\)}Z - An Optimizing {SMT} Solver},
  booktitle = {Proc.~TACAS 2015},
  OPTbooktitle = {Tools and Algorithms for the Construction and Analysis of
Systems
               - 21st International Conference, {TACAS} 2015, Held as
                 Part of the
               European Joint Conferences on Theory and Practice of
Software, {ETAPS}
               2015, London, UK, April 11-18, 2015. Proceedings},
  pages     = {194--199},
  year      = {2015},
  series    = LNCS,
  volume    = {9035},
  publisher = SV,
}

@inproceedings{GhilardiR:IJCAR10,
  author    = {Silvio Ghilardi and
               Silvio Ranise},
  title     = {{MCMT:} {A} Model Checker Modulo Theories},
  booktitle = {Proc.~IJCAR 2010},
  OPTbooktitle = {Automated Reasoning, 5th International Joint Conference,
{IJCAR} 2010,
               Edinburgh, UK, July 16-19, 2010. Proceedings},
  pages     = {22--29},
  year      = {2010},
  series    = LNCS,
  volume    = {6173},
  publisher = SV,
}

@article{HyvarinenJN:JSAT09,
  author    = {Antti Eero Johannes Hyv{\"{a}}rinen and
               Tommi A. Junttila and
               Ilkka Niemel{\"{a}}},
  title     = {Incorporating Clause Learning in Grid-Based Randomized
                {SAT} Solving},
  journal   = JSAT,
  volume    = {6},
  number    = {4},
  pages     = {223--244},
  year      = {2009},
}

@article{HyvarinenJN:FI11,
  author    = {Antti Eero Johannes Hyv{\"{a}}rinen and
               Tommi A. Junttila and
               Ilkka Niemel{\"{a}}},
  title     = {Partitioning Search Spaces of a Randomized Search},
  journal   = FI,
  volume    = {107},
  number    = {2-3},
  pages     = {289--311},
  year      = {2011},
}

@inproceedings{TakHB:SAT12,
  author    = {Peter van der Tak and
               Marijn Heule and
               Armin Biere},
  title     = {Concurrent Cube-and-Conquer - (Poster Presentation)},
  booktitle = {Proc.~SAT 2012},
  OPTbooktitle = {Theory and Applications of Satisfiability Testing - {SAT}
               2012 - 15th International Conference, Trento, Italy,
               June 17-20, 2012. Proceedings},
  pages     = {475--476},
  year      = {2012},
  series    = LNCS,
  volume    = {7317},
  publisher = SV,
}

@inproceedings{ChrabakhW:SC03,
  author    = {Wahid Chrabakh and
               Richard Wolski},
  title     = {{GridSAT}: {A} Chaff-based Distributed {SAT} Solver for the
Grid},
  booktitle = {Proc.~SC 2003},
  OPTbooktitle = {Proceedings of the {ACM/IEEE} {SC2003} Conference on High
Performance
               Networking and Computing, 15-21 November 2003, Phoenix,
AZ, USA, CD-Rom},
  pages     = {37},
  year      = {2003},
  publisher = ACM,
}

@inproceedings{HeuleKWB:HVC11,
  author    = {Marijn Heule and
               Oliver Kullmann and
               Siert Wieringa and
               Armin Biere},
  title     = {Cube and Conquer: Guiding {CDCL} {SAT} Solvers by
Lookaheads},
  booktitle = {Proc.~HVC 2011},
  OPTbooktitle = {Hardware and Software: Verification and Testing - 7th
International
               Haifa Verification Conference, {HVC} 2011, Haifa, Israel,
December
               6-8, 2011, Revised Selected Papers},
  pages     = {50--65},
  series    = LNCS,
  volume    = {7261},
  publisher = SV,
  year      = {2012},
}

@mastersthesis{Reisenberger:MsC2014,
  author    = {Christian Reisenberger},
  title     = {{PBoolector}: a Parallel {SMT} Solver for {QF\_BV} by
                Combining Bit-Blasting with Look-Ahead},
  school    = {Johannes Kepler Univesit\"{a}t Linz},
  address   = {Linz, Austria},
  year      = {2014},
}

@article{zhang:psato,
    author = {H. Zhang and M. Bonacina and J. Hsiang},
    title = {{PSATO}: {A} Distributed Propositional Prover and
                its Application to Quasigroup Problems},
    journal = JSC,
    volume = {21},
    number = {4},
    pages = {543--560},
    year = {1996},
    url = {citeseer.ist.psu.edu/zhang96psato.html}
}

@article{boehm:parallelsolver,
    author = {Max B{\"o}hm and Ewald Speckenmeyer},
    title = {A Fast Parallel {SAT}-solver: Efficient workload
        balancing},
    journal = AMAI,
    volume = {17},
    number = {4--3},
    year = {1996},
    pages = {381--400}
}

@inproceedings{DeharbeFMP:CADE11,
  author    = {David D{\'{e}}harbe and
               Pascal Fontaine and
               Stephan Merz and
               Bruno Woltzenlogel Paleo},
  title     = {Exploiting Symmetry in {SMT} Problems},
  OPTbooktitle = {Automated Deduction - {CADE-23} - 23rd International Conference on
               Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings},
  booktitle = {Proc.~CADE-13},
  pages     = {222--236},
  year      = {2011},
  series    = LNCS,
  volume    = {6803},
  publisher = SV,
}

@incollection{HeuleM09,
  author    = {Marijn Heule and
               Hans van Maaren},
  title     = {Look-Ahead Based {SAT} Solvers},
  booktitle = {Handbook of Satisfiability},
  pages     = {155--184},
  year      = {2009},
  OPTeditor    = {Armin Biere and
               Marijn Heule and
               Hans van Maaren and
               Toby Walsh},
  series    = {Frontiers in Artificial Intelligence and Applications},
  volume    = {185},
  publisher = {{IOS} Press},
  isbn      = {978-1-58603-929-5},
  timestamp = {Wed, 16 Sep 2009 11:21:15 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/series/faia/2009-185},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{SebastianiT12,
  author    = {Roberto Sebastiani and Silvia Tomasi},
  title     = {Optimization in {SMT} with {LA(Q)} Cost Functions},
  booktitle = {Proc. IJCAR 2012},
  OPTbooktitle = {Automated Reasoning - 6th International Joint Conference, {IJCAR}
               2012, Manchester, UK, June 26-29, 2012. Proceedings},
  pages     = {484--498},
  year      = {2012},
  series    = LNCS,
  volume    = {7364},
  publisher = SV,
}

@inproceedings{BCCFZ:DAC99,
  author    = {A. Biere and A. Cimatti and E.M. Clarke and M. Fujita and Y. Zhu},
  title     = {Symbolic Model Checking Using {SAT} Procedures instead of {BDDs}},
  booktitle = {DAC},
  year      = {1999},
  pages     = {317-320},
  ee        = {http://doi.acm.org/10.1145/309847.309942},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{BCCZ99,
  author         = {Armin Biere and Alessandro Cimatti and Edmund M.
                    Clarke and Yunshan Zhu},
  title          = {Symbolic Model Checking without {BDDs}},
  booktitle      = {Proc.~TACAS '99},
  series         = LNCS,
  publisher      = SV,
  volume         = {1579},
  year           = {1999},
  pages          = {193--207},
}


@inproceedings{HJMS:SPIN03,
  author    = {Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar and Gregoire Sutre},
  title     = {Software Verification with {Blast}},
  booktitle = {Tenth International Workshop on Model Checking of Software (SPIN)},
  series    = LNCS,
  volume    = {2648}, 
  publisher = SV, 
  year      = {2003}, 
  pages     = {235--239}
}

@inproceedings{DutertreM:CAV2006,
  author    = {Bruno Dutertre and Leonardo Mendon{\c{c}}a de Moura},
  title     = {A Fast Linear-Arithmetic Solver for {DPLL(T)}},
  booktitle = {Proc.~CAV 2006},
  pages     = {81--94},
  year      = {2006},
  volume    = {4144},
  series    = LNCS,
  publisher = SV,
}

@inproceedings{YordanovWHK:NFM13,
  author    = {Boyan Yordanov and
               Christoph M. Wintersteiger and
               Youssef Hamadi and
               Hillel Kugler},
  title     = {SMT-Based Analysis of Biological Computation},
  booktitle = {Proc.~NFM 2013},
  pages     = {78--92},
  year      = {2013},
  series    = LNCS,
  volume    = {7871},
  publisher = SV,
}

@article{SebastianiT:ACMTCL15,
  author    = {Roberto Sebastiani and Silvia Tomasi},
  title     = {Optimization Modulo Theories with Linear Rational Costs},
  journal   = {{ACM} Transactions on Computational Logic},
  volume    = {16},
  number    = {2},
  pages     = {12:1--12:43},
  year      = {2015},
}

@article{HyvarinenMS:SAT2015,
  author    = {Antti E. J. Hyv{\"a}rinen and Matteo Marescotti and
               Natasha Sharygina},
  title     = {Search-Space Partitioning for Parallelizing {SMT} Solvers},
  pages     = {369--386},
  year      = {2015},
  booktitle = {Proc.\ SAT 2015},
  volume    = {9340},
  series    = LNCS,
  publisher = SV,
}

@article{HyvarinenJN:SAT2006,
  author    = {Antti E. J. Hyv{\"a}rinen and Tommi Junttila and Ilkka
               Niemel{\"a}},
  title     = {A Distribution Method for Solving {SAT} in Grids},
  booktitle = {Proc.\ SAT 2006},
  pages     = {430--435},
  year      = {2006},
  series    = LNCS,
  volume    = {4121},
  publisher = SV,
}

@inproceedings{FSS_TACAS13,
    title        = {{eVolCheck}: Incremental Upgrade Checker for {C}},
    OPTbooktitle    = {19th International Conference on Tools and Algorithms
                    for the Construction and Analysis of Systems (TACAS 2013)},
    booktitle    = {Proc.~TACAS 2013},
    year         = {2013},
    pages        = {292-307},
    volume       = {7795},
    series       = LNCS,
    publisher    = SV,
    author       = {Grigory Fedyukovich and Ondrej Sery and Natasha Sharygina},
}

@inproceedings{SFS_ATVA12,
    author       = {Ondrej Sery and Grigory Fedyukovich and Natasha
                    Sharygina},
    title        = {{FunFrog}: Bounded Model Checking with Interpolation-based
                    Function Summarization},
    OPTbooktitle    = {The 10th International Symposium on Automated Technology for
                    Verification and Analysis (ATVA 2012)},
    booktitle    = {Proc.~ATVA 2012},
    pages        = {203-207},
    volume       = {7561},
    publisher    = SV,
    series       = LNCS,
    year         = {2012},
}

@inproceedings{RolliniAFHS:LPAR2013,
  author    = {Simone Fulvio Rollini and
               Leonardo Alt and
               Grigory Fedyukovich and
               Antti Eero Johannes Hyv{\"{a}}rinen and
               Natasha Sharygina},
  title     = {{PeRIPLO}: {A} Framework for Producing Effective
                Interpolants in {SAT}-Based Software Verification},
  OPTbooktitle = {Logic for Programming, Artificial Intelligence, and
                    Reasoning - 19th International Conference, LPAR-19,
                    Stellenbosch, South Africa, December
                    14-19, 2013. Proceedings},
  booktitle = {Proc.~LPAR 2013},
  pages     = {683--693},
  year      = {2013},
  series    = LNCS,
  volume    = {8312},
  publisher = SV,
}

@inproceedings{AltFHS:VSTTE2015,
  author    = {Leonardo Alt and
               Grigory Fedyukovich and
               Antti E. J. Hyv{\"{a}}rinen and
               Natasha Sharygina},
  title     = {A Proof-Sensitive Approach for Small Propositional Interpolants},
  OPTbooktitle = {Verified Software: Theories, Tools, and Experiments - 7th
                International Conference, {VSTTE} 2015, San Francisco, CA, USA, July
                18-19, 2015.  Revised Selected Papers},
  booktitle = {Proc.~VSTTE 2015},
  pages     = {1--18},
  series    = LNCS,
  volume    = {9593},
  publisher = SV,
  year      = {2016},
}

@article{HubermanLH_science97,
  author    = {Bernardo A. Huberman and Rajan M. Lukose and Tad Hogg},
  title     = {An Economics Approach to Hard Computational Problems},
  journal   = SCIENCE,
  volume    = {275},
  number    = {5296},
  pages     = {51--54},
  year      = {1997},
}

@inproceedings{JovanovicD:FMCAD16,
  author    = {Dejan Jovanovic and
               Bruno Dutertre},
  title     = {Property-directed k-induction},
  booktitle = {Proc.~FMCAD 2016},
  OPTbooktitle = {2016 Formal Methods in Computer-Aided Design, {FMCAD} 2016, Mountain
               View, CA, USA, October 3-6, 2016},
  pages     = {85--92},
  year      = {2016},
  OPTeditor    = {Ruzica Piskac and
               Muralidhar Talupur},
  publisher = {{IEEE}},
}

@inproceedings{AltHAS:FMCAD17,
  author    = {Leonardo Alt and
               Antti Eero Johannes Hyv{\"{a}}rinen and
               Sepideh Asadi and
               Natasha Sharygina},
  title     = {Duality-based interpolation for quantifier-free equalities and uninterpreted
               functions},
  booktitle = {Proc.~FMCAD 2017},
  OPTbooktitle = {2017 Formal Methods in Computer Aided Design, {FMCAD} 2017, Vienna,
               Austria, October 2-6, 2017},
  pages     = {39--46},
  year      = {2017},
  OPTeditor    = {Daryl Stewart and
               Georg Weissenbacher},
  publisher = {{IEEE}},
}

@inproceedings{DutertreM:CAV06,
  author    = {Bruno Dutertre and
               Leonardo Mendon{\c{c}}a de Moura},
  title     = {A Fast Linear-Arithmetic Solver for {DPLL(T)}},
  booktitle = {Proc.~CAV 2006},
  OPTbooktitle = {Computer Aided Verification, 18th International Conference, {CAV}
               2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
  pages     = {81--94},
  year      = {2006},
  OPTeditor    = {Thomas Ball and
               Robert B. Jones},
  series    = {LNCS},
  volume    = {4144},
  publisher = {Springer},
}


@article{DetlefsNS:JAC05,
  author    = {David Detlefs and
               Greg Nelson and
               James B. Saxe},
  title     = {Simplify: a theorem prover for program checking},
  journal   = {J. {ACM}},
  volume    = {52},
  number    = {3},
  pages     = {365--473},
  year      = {2005},
}


